COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	! Axioms for Zermelo-Fraenkel Set Theory    AJT June 75, modified JMC !
C00005 ENDMK
C⊗;
COMMENT	! Axioms for Zermelo-Fraenkel Set Theory    AJT June 75, modified JMC !

DECLARE INDCONST nl int;
DECLARE PREDCONST ε 2[INF];
DECLARE PREDCONST ⊂ 2[INF];
DECLARE OPCONST ∪ 2[INF];
DECLARE OPCONST ∩ 2[INF];
DECLARE OPCONST union 1[pre];
DECLARE OPCONST intersect 1[pre];
DECLARE INDVAR r s t u v w x y z;
DECLARE PREDPAR A 2 B 1;

AXIOM ZF:
	EXT: 	∀x y.(∀z.(zεx≡zεy)≡x=y);        	% Extensionality 
	EMT: 	∀y.¬yεnl;				% Null set 
	PAIR: 	∀x y w.(wε{x,y}≡w=x∨w=y);		% Unordered pair 
	UNION: 	∀x z.(zεunion(x)≡∃t.(tεx∧zεt));		% Sum set 
	INTERSECT: 	∀x z.(zεintersect(x)≡∀t.(tεx⊃zεt));	% Product set 
	INF: 	(0εint∧∀y.(yεint⊃(y∪{y})εint));		% Infinity 
	INDUCT:	B(0)∧∀x.(xεint∧B(x)⊃B(x∪{x}))⊃∀x.(xεint⊃B(x)); % Induction
	REPL:	∀x.∃y.∀z.(A(x,z)≡y=z) ⊃			% Replacement
			∀u.∃v.(∀r.(rεv ≡ ∃s.(sεu∧A(s,r))));
	SEP:	∀x.∃y.∀z.(zεy≡zεx∧B(z));		% Separation
	POWER:	∀x.∃y.∀z.(zεy≡z⊂x);			% Power set 
	REG:	∀x.∃y.(x=0∨(yεx∧∀z.(zεx⊃¬zεy)));;;	% Regularity 


DECLARE PREDCONST FUN 1,INTO 2,PSUBSET 2[INF];
DECLARE	OPCONST rng 1 dom 1;

AXIOM
	SUBSET:		∀x y.(x⊂y≡∀z.(zεx⊃zεy));
	PROPSUBSET:	∀x y.(PSUBSET(x,y)≡x⊂y∧¬x=y);
	PAIRFUN:     	∀x y z.(zε{x,y}≡z=x∨z=y);
	UNITSETFUN:	∀x.( {x}={x,x} );
	OPAIRFUN:	∀x y.( <x,y>={{x},{x,y}} );
	FUNCTION:	∀w.(FUN(w)≡∀z.(zεw⊃∃x y.(z=<x,y>))∧
			   ∀x y z.(<x,y>εw∧<x,z>εw⊃y=z) );
	DOMAIN:		∀w x.(xεdom(w)≡FUN(w)∧∃y z.(yεw∧y=<x,z>));
	RANGE:		∀w x.(xεrng(w)≡FUN(w)∧∃y z.(yεw∧y=<z,x>));
	INTO:           ∀w x.(INTO(w,x)≡rng(w)⊂x);
	SUM:		∀x y z.(zεx∪y≡zεx∨zεy);
	PRODUCT:	∀x y z.(zεx∩y≡zεx∧zεy); ;